a, b:Atom2. a = b  a =a2 b 

latex

Definitions	x:AB(x), P  Q, P & Q, Prop, Type, s = t, Atom$n, b, eq_atom$n(x;y), x:A. B(x), t  T, P  Q, P  Q
Lemmas	eq atom wf2, assert wf, assert of eq atom2